x,y:. (x <z y)  (x < y) 

latex

ProofTree

Definitions	, t  T, P  Q, P  Q, P  Q, P  Q, x:A. B(x), True, T, i <z j, P  Q, Dec(P), False, A
Lemmas	lt int wf, assert wf, decidable lt, bfalse wf, bool wf, true wf, squash wf, assert of ff, btrue wf, assert of tt